package kodkod.ast.visitor.graph;

import java.io.File;
import java.util.*;

import kodkod.analysis.Problem;
import kodkod.ast.*;
import kodkod.ast.operator.*;
import kodkod.engine.fol2sat.Translation;

public class ReducedAST extends GraphVisitorDOT {

	public ReducedAST(File file, Problem problem) {
		super(file);
	}
	
	protected HashMap<Node, Node> childParent = new HashMap<Node, Node>();
	
	protected HashSet<UndirectedEdge> edgeList = new HashSet<UndirectedEdge>();
	
	@Override
	protected void newEdge(Node parent, Node child) {
//		UndirectedEdge edge = new UndirectedEdge(parent.toString(), child.toString());
//		if (!edgeList.add(edge)) return;
		
		super.newEdge(parent, child);
	}
		
	public void visit(BinaryExpression node) {
		if (node.op().equals(ExprOperator.JOIN)) {
			ArrayList<Expression> joinedExpressions = collectAllExpressionsByType(node, ExprOperator.JOIN);
			for (Expression e : joinedExpressions) {
				newEdge(node, e);
				e.accept(this);
			}
		}
		
		else if (node.op().equals(ExprOperator.UNION)) {
			ArrayList<Expression> joinedExpressions = collectAllExpressionsByType(node, ExprOperator.UNION);
			for (Expression e : joinedExpressions) {
				newEdge(node, e);
				e.accept(this);
			}
		}
		
		else {
			super.visit(node);
		}
	}
	
	public void visit(BinaryFormula node) {
		if (node.op().equals(FormulaOperator.AND)) {
			ArrayList<Formula> joinedFormulas = collectAllFormulasByType(node, FormulaOperator.AND);
			for (Formula f : joinedFormulas) {
				newEdge(node, f);
				f.accept(this);
			}
		}
		
		else if (node.op().equals(FormulaOperator.OR)) {
			ArrayList<Formula> joinedFormulas = collectAllFormulasByType(node, FormulaOperator.OR);
			for (Formula f : joinedFormulas) {
				newEdge(node, f);
				f.accept(this);
			}
		}
		
		else {
			super.visit(node);
		}
	}

	private ArrayList<Expression> collectAllExpressionsByType(BinaryExpression node, ExprOperator optype) {
		ArrayList<Expression> list = new ArrayList<Expression>();
		
		Expression check = node.left();
		
		if (check instanceof UnaryExpression && ((UnaryExpression)check).op().equals(ExprOperator.TRANSPOSE)) {
			check = ((UnaryExpression)check).expression();
		}
		
		if (check instanceof BinaryExpression && ((BinaryExpression)check).op().equals(optype)) {
			list.addAll(collectAllExpressionsByType((BinaryExpression)check, optype));
		} else {
			list.add(check);
		}
		
		check = node.right();
		
		if (check instanceof UnaryExpression && ((UnaryExpression)check).op().equals(ExprOperator.TRANSPOSE)) {
			check = ((UnaryExpression)check).expression();
		}
		
		if (check instanceof BinaryExpression && ((BinaryExpression)check).op().equals(optype)) {
			list.addAll(collectAllExpressionsByType((BinaryExpression)check, optype));
		} else {
			list.add(check);
		}
		
		return list;
	}
	
	
	private ArrayList<Formula> collectAllFormulasByType(BinaryFormula node, FormulaOperator optype) {
		ArrayList<Formula> list = new ArrayList<Formula>();
		
		Formula check = node.left();
				
		if (check instanceof BinaryFormula && ((BinaryFormula)check).op().equals(optype)) {
			list.addAll(collectAllFormulasByType((BinaryFormula)check, optype));
		} else {
			list.add(check);
		}
		
		check = node.right();
				
		if (check instanceof BinaryFormula && ((BinaryFormula)check).op().equals(optype)) {
			list.addAll(collectAllFormulasByType((BinaryFormula)check, optype));
		} else {
			list.add(check);
		}
		
		return list;
	}

}

class UndirectedEdge {
	public String a, b;
	public UndirectedEdge(String a, String b) {
		this.a = a;
		this.b = b;
	}
	
	public boolean equals(Object o) {
		if (o == null) {
			return false;
		}
		if (o instanceof UndirectedEdge) {
			UndirectedEdge edge = (UndirectedEdge)o;
			return a.equals(a) && b.equals(b) || a.equals(b) && b.equals(a);
		} else {
			return false;
		}
	}
	
	public int hashCode() {
		return a.hashCode() + b.hashCode();
	}
}